\begin{tabbing}
ecl{-}trans{-}normal($x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$spreadn(\=$x$;\+
\\[0ex]$T$,${\it ks}$,$i$,$g$,$h$,$a$,$e$.((($\forall$$x$,$y$:$T$. decidable(($x$ = $y$))) $\wedge$ ($\forall$$n$:$\mathbb{N}$. $\neg$($\uparrow$($h$($n$,$i$)))))
\\[0ex]$\wedge$ finite{-}type($T$)
\\[0ex]$\wedge$ sorted($e$)
\\[0ex]$\wedge$ no\_repeats($\mathbb{N}^{+}$; $e$)))
\-
\end{tabbing}